(* SPDX-License-Identifier: GPL-2.0 or GPL-3.0
   Copyright © 2019 Ariadne Devos *)

Require Import S.Vector.Fold.
Require Import S.Vector.Iota.
Require Import S.Vector.Bounds.
Require Import Coq.Arith.PeanoNat.
Require Import Coq.Lists.List.
Require Import Coq.omega.Omega.

(* Positional number systems (most-significant to least-significant).
   Direction: from text to numbers.
   Features: bounds information *)

Definition positional_value radix digits : nat
  := let n := length digits in
     let exponents := countdown n in
     let weights := map (Nat.pow radix) exponents in
     let parts := map (prod_curry Nat.mul) (combine digits weights) in
     all nat plus 0 parts.

Lemma positional_value_test0 : positional_value 2 nil = 0.
Proof. compute. reflexivity. Qed.

Lemma positional_value_test1 : positional_value 3 (1 :: 2 :: 0 :: nil) = 15.
Proof. compute. reflexivity. Qed.

Lemma positional_value_test2 : positional_value 3 (0 :: 2 :: 0 :: nil) = 6.
Proof. compute. reflexivity. Qed.

Theorem positional_value_peel radix a digits
  : positional_value radix (a :: digits)
    = a * radix ^ length digits + positional_value radix digits.
Proof.
  reflexivity.
  (* That was easy! Partially computable functions are very practical. *)
Qed.

Theorem positional_value_bounds (radix : nat) (digits : list nat)
  : 1 < radix -> vector_lt_constant radix digits -> positional_value radix digits < Nat.pow radix (length digits).
Proof.
  intro P.
  induction digits.
  + cbn.
    intro Q.
    apply Nat.lt_0_1.
  + rewrite vector_lt_peell.
    rewrite positional_value_peel.
    intuition.
    set (x := radix ^ length (a :: digits)).
    cbn in x.
    subst x.
    (* now solve this system *)
    rewrite Nat.lt_add_lt_sub_l.
    rewrite <- Nat.mul_sub_distr_r.
    assert (T : 0 < radix - a).
    2 : apply (lt_le_trans _ (1 * radix ^ length digits)).
    3 : apply mult_le_compat_r.
    all : omega.
Qed.

